natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
model category, model -category
Definitions
Morphisms
Universal constructions
Refinements
Producing new model structures
Presentation of -categories
Model structures
for -groupoids
on chain complexes/model structure on cosimplicial abelian groups
related by the Dold-Kan correspondence
for equivariant -groupoids
for rational -groupoids
for rational equivariant -groupoids
for -groupoids
for -groups
for -algebras
general -algebras
specific -algebras
for stable/spectrum objects
for -categories
for stable -categories
for -operads
for -categories
for -sheaves / -stacks
These exist a class of model category structures on certain categories of cubical sets, due to Christian Sattler, motivated by cubical type theory.
Let be a small category with finite products. Assume there is a (cartesian) interval object , i.e., an object with two parallel morphisms , where is the terminal object in .
Assume further that we have connection maps such that and .
We also need a face lattice , that is, a sub-lattice of the subobject classifier in the presheaf category containing the endpoints of each cylinder object for each object of , and an operation right adjoint to the projection in the sense that iff , where .
If we want the model to be effective, we also require that each proposition with is decidable. (This rules out taking .)
A simple and central example is the full subcategory of the category of posets on powers of . This is also the Lawvere theory of distributive lattices. The idempotent completion is the full subcategory of on finite lattices.
Other prominent examples are the Lawvere theories of de Morgan, Kleene, and boolean algebras.
For computational purposes we can take to be the smallest lattice containing the cylinder endpoints (the faces of cubes). To get Cisinski model structures we can take .
One may wonder whether these models structures are equivalent to the model in simplicial sets. This is not the case for Cartesian cubes; see mailing-list. However, this model does form a Grothendieck (infinity,1)-topos, because it satisfies the Giraud axioms. For deMorgan cubical sets the geometric realization is not a Quillen equivalence (because of the reversal map); the counterexample is the unit interval quotient by the symmetry); see Sattler. Whether they are equivalent by another map is not yet excluded. The question whether the geometric realization for the cubical sets based on distributive lattices is an equivalence is still open, cf. also Hackney and Rovelli and Streicher and Weinberger.
Thierry Coquand, A model structure on some presheaf categories, pdf
Thierry Coquand, Some examples of complete Cisinski model structures, pdf
Christian Sattler, Do cubical models of type theory also model homotopy types, lecture at Hausdorff Trimester Program: Types, Sets and Constructions, youtube
Philip Hackney and Martina Rovelli, Induced model structures for ∞-categories and ∞-groupoids, arXiv:2102.01104, Proc. Amer. Math. Soc., June 10, 2022
Thomas Streicher and Jonathan Weinberger, Simplicial sets inside cubical sets arXiv:1911.09594, Theory and Applications of Categories, Vol. 37, 2021, No. 10, pp 276–286
Last revised on August 15, 2022 at 02:31:51. See the history of this page for a list of all contributions to it.